perm filename PCHECK.LAP[CHE,WD] blob
sn#032194 filedate 1973-03-28 generic text, type T, neo UTF8
(LAP DELETEPROP SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 1.)
TAG1 (HRRZ@ 1. 0. P)
(JUMPE 1. TAG3)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CAME 1. -1. P)
(JRST 0. TAG7)
(HRRZ@ 1. 0. P)
(CALL 1. (E CDDR))
(HRRM@ 1. 0. P)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG2)
TAG7 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP GETGET SUBR)
(PUSH P 1.)
(PUSH P 2.)
(HRRZ@ 1. 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -1. P)
(JUMPE 1. TAG3)
(MOVE 2. -2. P)
(HLRZ@ 1. 1.)
(CALL 2. (E SEEKPROP))
(MOVEM 1. 0. P)
(JUMPE 1. TAG7)
(JRST 0. TAG2)
TAG7 (HRRZ@ 1. -1. P)
(HRRZ@ 1. 1.)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INITPROP SUBR)
(PUSH P 2.)
(HRRZ@ 2. 1.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVE 2. 3.)
(CALL 2. (E XCONS))
(HRRM@ 1. 0. P)
(POP P 1.)
(POPJ P)
NIL
(LAP SEEKPROP SUBR)
(PUSH P 1.)
(PUSH P 2.)
(MOVE 1. 2.)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E GETL))
(PUSH P 1.)
(JUMPE 1. TAG2)
(JRST 0. TAG1)
TAG2 (MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP AE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE AND))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (FIRST ARG IS NOT AN AND)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E ANDELIM1))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE AE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP AI FSUBR)
(PUSH P 1.)
(CALL 1. (E WFFLIST))
(CALL 1. (E CONJOIN))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE AI))
(CALL 2. (E CONS))
(EXCH 1. -1. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP ALT FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ALT1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (LINES ARE NOT ALTERNATIVES)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE ALT))
(CALL 2. (E CONS))
(CALL 1. (E NCONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ASS FSUBR)
(MOVEI 2. (QUOTE ASS))
(PUSH P 1.)
(CALL 2. (E XCONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(CALL 0. (E NEXTLINE))
(CALL 1. (E NCONS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(JCALL 3. (E ADDLINE))
NIL
(LAP BS FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E MAKECONSES))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E BOUNDSUBST))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE BS))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP DED FSUBR)
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NOTHING TO CONCLUDE)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 1. 0. P)
(CALL 1. (E WFFLIST))
(CALL 1. (E CONJOIN))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E WFFPART))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE IMPLIES))
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DED))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(HRRZ@ 2. -2. P)
(CALL 2. (E SETDIF))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP DEF FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NAMES MUST BE ATOMS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE SETQ))
(CALL 2. (E CONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DEF))
(CALL 2. (E CONS))
(PUSH P 1.)
(CALL 0. (E NEXTLINE))
(CALL 1. (E NCONS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP DNE FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E DOUBLENEG))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO DOUBLE NEGATIVE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE DNE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP DNI FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE NOT))
(CALL 2. (E XCONS))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE NOT))
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DNI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP EG FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E EXGEN1))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE EG))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP ELIM FSUBR)
(PUSH P 1.)
(CALL 1. (E CADR))
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE SETQ))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO DEFINITION)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E CADR))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E SUBST))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE ELIM))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E SETDIF))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EQE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE EQUIVALENT))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO EQUIVALENCE)))
(CALL 1. (E ERREND))
TAG5 (MOVEI 2. (QUOTE 2.))
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(HRRZ@ 1. 0. P)
(CALL 1. (E REVERSE))
(JRST 0. TAG6)
TAG7 (HRRZ@ 1. 0. P)
TAG8
TAG6 (MOVEI 2. (QUOTE IMPLIES))
(MOVEM 1. 0. P)
(CALL 2. (E XCONS))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE EQE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EQI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E EQI1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (ARE NOT EQUIVALENT)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE EQI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ES FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E SPECALL))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE ES))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP IFE FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E IFE1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO IF /- THEN /- ELSE EXPRESSION)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE IFE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP IFI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E IFI1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE IFI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP LC FSUBR)
(PUSH P 1.)
(CALL 1. (E LAMEXP))
(CALL 1. (E NCONS))
(MOVE 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE EQUAL))
(CALL 2. (E XCONS))
(POP P 2.)
(PUSH P 1.)
(MOVEI 1. (QUOTE LC))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(JCALL 3. (E ADDLINE))
NIL
(LAP MP FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E MP1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (CANNOT MODUS PONENS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE MP))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP NE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E NOTELIM))
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO CONTRADICTION)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE NE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVEI 1. (QUOTE FALSE))
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP NI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E NOTINTRO))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO IMPLIES FALSE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE NI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP OE FSUBR)
(PUSH P 1.)
(JUMPE 1. TAG6)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG5)
TAG6 (MOVEI 1. (QUOTE (NEED AT LEAST TWO ARGS)))
(CALL 1. (E ERREND))
TAG5 (HLRZ@ 1. 0. P)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E WFFLIST))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ORELIM1))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE OE))
(CALL 2. (E CONS))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP OI FSUBR)
(PUSH P 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPN 1. TAG7)
(MOVE 1. 0. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO VALID PROPOSITION)))
(CALL 1. (E ERREND))
(JRST 0. TAG8)
TAG9 (JRST 0. TAG2)
TAG8
TAG7 (HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG12)
(MOVE 1. 0. P)
(JUMPN 1. TAG14)
(HLRZ@ 1. -3. P)
(MOVEM 1. 0. P)
TAG14
TAG12 (HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG16)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 2. -1. P)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
(JRST 0. TAG15)
TAG16 (MOVE 2. -1. P)
(HLRZ@ 1. -3. P)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
TAG17
TAG15 (HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. -1. P)
(JUMPN 1. TAG20)
(HLRZ@ 1. -1. P)
(JRST 0. TAG19)
TAG20 (MOVE 1. -1. P)
(CALL 1. (E REVERSE))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
TAG21
TAG19 (MOVE 2. -2. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE OI))
(CALL 2. (E CONS))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP REP FSUBR)
(PUSH P 1.)
(CALL 1. (E CADR))
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ISEQUIVALENCE))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO EQUATION)))
(CALL 1. (E ERREND))
TAG5 (MOVEI 2. (QUOTE 2.))
(HRRZ@ 1. -1. P)
(CALL 1. (E CADR))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(HRRZ@ 1. 0. P)
(CALL 1. (E REVERSE))
(JRST 0. TAG6)
TAG7 (HRRZ@ 1. 0. P)
TAG8
TAG6 (MOVEM 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E SUBST))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE REP))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP REPL FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 4. -1. P)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(MOVEI 3. (QUOTE T))
(MOVE 2. 1.)
(POP P 1.)
(CALL 4. (E REPEITHER))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE REPL))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP REPR FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 4. -1. P)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 4. (E REPEITHER))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE REPR))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP TAUT FSUBR)
(PUSH P 1.)
(HRRZ@ 1. 1.)
(CALL 1. (E WFFLIST))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E NCONS))
(MOVE 4. 1.)
(POP P 3.)
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE NIL))
(CALL 4. (E TH1))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (DOES NOT FOLLOW)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE TAUT))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP UG FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(PUSH P 1.)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG5)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (ILLEGAL ARGUMENT)))
(CALL 1. (E ERREND))
TAG2 (HLRZ@ 4. 0. P)
(HLRZ@ 3. 0. P)
(MOVE 2. -1. P)
(MOVE 1. -2. P)
(CALL 4. (E UNGEN))
(MOVEM 1. -2. P)
(JRST 0. TAG4)
TAG3 (HLRZ@ 4. 0. P)
(HRRZ@ 4. 4.)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(HLRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(MOVE 2. -1. P)
(MOVE 1. -2. P)
(CALL 4. (E UNGEN))
(MOVEM 1. -2. P)
TAG4 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG5 (MOVE 2. -3. P)
(MOVEI 1. (QUOTE UG))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. -2. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP US FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E SPECALL))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE US))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP USEAX FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE AXIOM))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH AXIOM)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E SPECALL))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE USEAX))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP USESCHM FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE SCHEMA))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (IS NOT SCHEMA)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 3. 0. P)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 3. (E PROPSUBST))
(CALL 1. (E LAMEXP))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE USESCHM))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP USETHM FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE THEOREM))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH THEOREM)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E SPECALL))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE USETHM))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP BT FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *DIF))
(JRST 0. TAG4)
TAG5 (HLRZ@ 1. -1. P)
TAG6
TAG4 (MOVEM 1. -1. P)
(CALL 0. (E CURTEXT))
(MOVEM 1. 0. P)
(CALL 0. (E CURLINE))
(MOVE 2. -1. P)
(CALL 2. (E *LESS))
(JUMPN 1. TAG10)
(MOVEI 2. (QUOTE 0.))
(MOVE 1. -1. P)
(CALL 2. (E *LESS))
(JUMPE 1. TAG9)
TAG10 (MOVEI 1. (QUOTE (NON EXISTANT LINE)))
(CALL 1. (E ERREND))
TAG9 (MOVEI 2. (QUOTE 0.))
(MOVE 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG12)
(CALL 0. (E CURPROOF))
(MOVEI 3. (QUOTE PROOF))
(MOVEI 2. (QUOTE NIL))
(CALL 3. (E PUTPROP))
(JRST 0. TAG11)
TAG12 (MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E NTHCDR))
(HLLZS@ 0. 1.)
(CALL 0. (E CURPROOF))
(MOVEI 3. (QUOTE PROOF))
(MOVE 2. 0. P)
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
TAG13
TAG11 (CALL 0. (E CURPROOF))
(CALL 1. (E INITPROOF))
(CALL 0. (E SHOWCURLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP FINDL FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HRRZ@ 1. -3. P)
(JUMPE 1. TAG6)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(JRST 0. TAG5)
TAG6 (CALL 0. (E CURPROOF))
TAG7
TAG5 (MOVEI 2. (QUOTE PROOF))
(MOVEM 1. 0. P)
(CALL 2. (E GET))
(MOVEM 1. -1. P)
TAG1 (MOVE 1. -1. P)
(JUMPE 1. TAG3)
(HLRZ@ 2. 1.)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(MOVE 1. -2. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG11)
(HLRZ@ 1. -1. P)
(CALL 1. (E SHOWLINE))
TAG11 (HRRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP GIVEAX FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC AXIOM NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL AXIOMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL AXIOMS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL AXIOMS))
TAG7 (MOVEI 3. (QUOTE AXIOM))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG9)
(HLRZ@ 1. 0. P)
(CALL 1. (E SHOWAXIOM))
TAG9 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP GIVESCHM FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC SCHEMA NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL SCHEMAS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL SCHEMAS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL SCHEMAS))
TAG7 (MOVEI 3. (QUOTE SCHEMA))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG9)
(HLRZ@ 1. 0. P)
(CALL 1. (E SHOWSCHEMA))
TAG9 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INVENTORY SUBR)
(MOVE 1. (SPECIAL AXIOMS))
(JUMPE 1. TAG5)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE AXIOMS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL AXIOMS))
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
TAG5 (MOVE 1. (SPECIAL SCHEMAS))
(JUMPE 1. TAG10)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE SCHEMAS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL SCHEMAS))
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
TAG10 (MOVE 1. (SPECIAL PROOFS))
(JUMPE 1. TAG15)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE PROOFS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL PROOFS))
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
TAG15 (MOVE 1. (SPECIAL THEOREMS))
(JUMPE 1. TAG20)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE THEOREMS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL THEOREMS))
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
TAG20 (MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP MAKETHM FSUBR)
(PUSH P 1.)
(CALL 1. (E CADR))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HRRZ@ 1. 1.)
(JUMPE 1. TAG2)
(HRRZ@ 3. -2. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(JRST 0. TAG1)
TAG2 (CALL 0. (E CURPROOF))
(MOVE 3. 1.)
TAG3
TAG1 (MOVE 2. -1. P)
(POP P 1.)
(SUB P (C 0. 0. 2. 2.))
(JCALL 3. (E MAKETHEOREM1))
NIL
(LAP ONDD SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL DDWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONIII SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL IIIWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONIMLAC SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL IMLACWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONTTY SUBR)
(CALL 0. (E INITTTYCHARSET))
(MOVE 1. (SPECIAL TTYWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP PROOF FSUBR)
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO NAME GIVEN)))
(CALL 1. (E ERREND))
TAG5 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG7)
(MOVEI 1. (QUOTE (NON ATOMIC PROOF NAME)))
(CALL 1. (E ERREND))
TAG7 (HLRZ@ 1. 0. P)
(CALL 1. (E INITPROOF))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG9)
(CALL 0. (E SHOWCURLINE))
TAG9 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP REDO FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(POP P 2.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG7)
(MOVEI 1. (QUOTE (CANNOT REDO)))
(CALL 1. (E ERREND))
TAG7 (HRRZ@ 2. -4. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE 1.))
(MOVEM 1. 0. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E *PLUS))
(MOVEM 1. -1. P)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *PLUS))
(MOVEM 1. -2. P)
TAG1 (MOVE 1. -1. P)
(CAMN 1. -2. P)
(JRST 0. TAG4)
(CALL 1. (E BYPART))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(MOVEM 1. -3. P)
(MOVE 1. -1. P)
(CALL 1. (E BYPART))
(MOVE 2. -3. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVE 1. -3. P)
(CALL 1. (E *EVAL))
TAG10 (CALL 0. (E CURLINE))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG2 (MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG4 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP RESTOREALL FSUBR)
(JSP 6. SPECBIND)
(0. 0. (SPECIAL *PRINT))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVE 1. (SPECIAL *FILEPRINT))
(JUMPE 1. TAG11)
(MOVEI 1. (QUOTE T))
(MOVEM 1. (SPECIAL *PRINT))
(MOVEI 1. (QUOTE NIL))
TAG11 (MOVEI 1. (QUOTE DSK:))
(MOVEM 1. 0. P)
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG6)
(HLRZ@ 1. 1.)
(MOVEM 1. -1. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE OR DEVICE NAME)))
(CALL 1. (E ERREND))
TAG2 (MOVE 1. -1. P)
(CALL 1. (E NCONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E READIN))
(JRST 0. TAG5)
TAG3 (HRRZ@ 2. -1. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
(JRST 0. TAG2)
TAG4 (HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(MOVEM 1. 0. P)
(JRST 0. TAG5)
TAG5 (HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG6 (CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(JRST 0. SPECSTR)
NIL
(LAP SAVEALL FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK:) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (DEVICE BUT NO FILE)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(MOVEM 1. -1. P)
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SAVEAXIOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SAVESCHEMA))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SAVEPROOF))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SAVETHEOREM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SAVECOMS FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK:) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO FILE SPECIFIED)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(MOVEM 1. -1. P)
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SAVEAXCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SAVESCHMCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SAVEPRFCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SAVETHMCOM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SHOW FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPN 1. TAG12)
(CALL 0. (E CURPROOF))
(CALL 1. (E SHOWPROOF))
(JRST 0. TAG8)
TAG12
TAG2 (MOVE 1. -3. P)
(JUMPE 1. TAG7)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG6)
(HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE IMAGE))
(HLRZ@ 1. -3. P)
(CALL 2. (E GETGET))
(MOVEM 1. -2. P)
(JUMPN 1. TAG17)
(MOVEI 1. (QUOTE (NOTHING TO SHOW)))
(CALL 1. (E ERREND))
TAG17 (HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALLF@ 1. 0. P)
(SUB P (C 0. 0. 1. 1.))
TAG3 (HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG2)
TAG4 (HLRZ@ 1. -3. P)
(MOVEM 1. 0. P)
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JUMPE 1. TAG20)
(HLRZ@ 1. 1.)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG19)
TAG20 (MOVE 1. 0. P)
(MOVEM 1. -1. P)
(JRST 0. TAG18)
TAG19 (HLRZ@ 1. -3. P)
(MOVEM 1. -1. P)
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(MOVEI 1. (QUOTE NIL))
TAG21
TAG18
TAG5 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E *GREAT))
(JUMPN 1. TAG7)
(MOVE 1. 0. P)
(CALL 1. (E GETLINE))
(CALL 1. (E SHOWLINE))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. 0. P)
(CALL 2. (E *PLUS))
(MOVEM 1. 0. P)
(JRST 0. TAG5)
TAG6 (MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG28)
(MOVEI 1. (QUOTE (NEED NAME OR FILE SPEC)))
(CALL 1. (E ERREND))
TAG28 (HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG7 (MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(MOVEI 1. (QUOTE NIL))
TAG8 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP SHOWALL FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK:) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO FILE SPECIFIED)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(MOVEM 1. -1. P)
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SHOWAXIOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SHOWSCHEMA))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SHOWPROOF))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SHOWTHEOREM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SSEX FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG8)
(CALL 0. (E CURPROOF))
(JRST 0. TAG7)
TAG8 (HLRZ@ 1. -3. P)
TAG9
TAG7 (MOVEI 2. (QUOTE (PROOF)))
(MOVEM 1. -1. P)
(CALL 2. (E GETL))
(MOVEM 1. -2. P)
(JUMPN 1. TAG12)
(MOVEI 1. (QUOTE (NO PROOF BY THAT NAME)))
(CALL 1. (E ERREND))
TAG12 (HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(MOVEM 1. -2. P)
(MOVEI 1. (QUOTE PROOF))
(CALL 1. (E PRINT))
(MOVE 1. -1. P)
(CALL 1. (E PRINS))
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG5)
(HLRZ@ 1. 1.)
(MOVEM 1. 0. P)
(CALL 0. (E TERPRI))
(HLRZ@ 1. 0. P)
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVEI 3. (QUOTE 0.))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 6.))
(CALL 2. (E *PLUS))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(POP P 2.)
(CALL 2. (E *LESS))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE BY))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(JUMPE 1. TAG16)
(MOVEI 1. (QUOTE ASS))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(CALL 1. (E PRIN1))
(MOVEI 1. (QUOTE NIL))
TAG16
TAG2 (HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE 4.))
(MOVEI 1. (QUOTE //))
(CALL 2. (E PRINTN))
(MOVEI 1. (QUOTE BY))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVEI 3. (QUOTE 0.))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(JUMPE 1. TAG2)
(CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE 4.))
(MOVEI 1. (QUOTE //))
(CALL 2. (E PRINTN))
(MOVEI 1. (QUOTE ASS))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(CALL 1. (E PRINS))
(JRST 0. TAG2)
TAG5 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP ADDLINE SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 0. (E CURPROOF))
(PUSH P 1.)
(PUSH P (C 0. 0. TAG4 0.))
(CALL 0. (E CURTEXT))
(PUSH P 1.)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *PLUS))
(PUSH P 1.)
(MOVE 1. -4. P)
(CALL 1. (E NCONS))
(MOVE 2. -5. P)
(CALL 2. (E XCONS))
(MOVE 2. -6. P)
(CALL 2. (E XCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(CALL 1. (E NCONS))
(PUSH P 1.)
(MOVNI 6. 2.)
(JCALL 14. (E NCONC))
TAG4 (MOVEI 3. (QUOTE PROOF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PUTPROP))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. (SPECIAL CURLIN))
(CALL 2. (E *PLUS))
(MOVEM 1. (SPECIAL CURLIN))
(CALL 0. (E CURLINE))
(MOVEI 3. (QUOTE NEWNAM))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE /@))
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG6)
(CALL 0. (E SHOWCURLINE))
TAG6 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP ADDAXIOM FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE AXIOM))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL AXIOMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ADDSCHEMA FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE SCHEMA))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL SCHEMAS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ADDTHEOREM FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE THEOREM))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL THEOREMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ALPHAPART SUBR)
(PUSH P 1.)
(CALL 1. (E EXPLODE))
(CALL 1. (E REVERSE))
(PUSH P 1.)
TAG1 (HLRZ@ 1. 0. P)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG6)
(MOVE 1. 0. P)
(CALL 1. (E REVERSE))
(CALL 1. (E READLIST))
(JRST 0. TAG2)
TAG6 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALLVARS SUBR)
(MOVEI 2. (QUOTE NIL))
(JCALL 2. (E ALLVARS1))
NIL
(LAP ALLVARS1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. -1. P)
(CALL 1. (E ISVAR))
(JUMPE 1. TAG4)
(MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG6)
(MOVE 1. 0. P)
(JRST 0. TAG5)
TAG6 (MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E CONS))
TAG7
TAG5 (JRST 0. TAG3)
TAG4 (MOVE 1. 0. P)
TAG9
TAG3 (JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(HRRZ@ 1. -1. P)
(CALL 2. (E ALLVARSL))
TAG11
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALLVARSL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(JUMPN 1. TAG2)
(MOVE 1. 2.)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. -1. P)
(MOVE 2. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(CALL 2. (E ALLVARSL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ALLVARS1))
TAG3
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALT1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ)))
(CALL 3. (E INST))
(POP P 2.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ)))
(CALL 3. (E INST))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE INVALID))
TAG4
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ANDELIM1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(HRRZ@ 1. 1.)
(CALL 1. (E LENGTH))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVEI 2. (QUOTE AND))
(HLRZ@ 1. -3. P)
(CALL 2. (E NEQ))
(JUMPE 1. TAG6)
(MOVEI 1. (QUOTE (FIRST ARG IS NOT AN AND)))
(CALL 1. (E ERREND))
TAG6
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG8)
(MOVE 1. 0. P)
(CALL 1. (E REVERSE))
(CALL 1. (E CONJOIN))
(JRST 0. TAG2)
TAG8 (MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 2. (E *GREAT))
(JUMPE 1. TAG10)
(MOVEI 1. (QUOTE (TOO FEW CONJUNCTS)))
(CALL 1. (E ERREND))
TAG10 (HLRZ@ 2. -2. P)
(HRRZ@ 1. -3. P)
(CALL 2. (E NTHELT))
(MOVE 2. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP ASSLIST SUBR)
(MOVE 2. 1.)
(MOVEI 1. (QUOTE ASSPART))
(JCALL 2. (E MAPCAR))
NIL
(LAP ASSOCR SUBR)
(PUSH P 1.)
(PUSH P 2.)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG3)
(CALL 1. (E CDAR))
(CAME 1. -1. P)
(JRST 0. TAG7)
(HLRZ@ 1. 0. P)
(JRST 0. TAG2)
TAG7 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ASSPART SUBR)
(CALL 1. (E GETLINE))
(JCALL 1. (E CADDDR))
NIL
(LAP BINAND SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (AND TRUE TRUE)))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE TRUE))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE AND))
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG3 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG4)
(MOVE 2. 0. P)
(MOVEI 1. (QUOTE AND))
(CALL 2. (E CONS))
(JRST 0. TAG1)
TAG4 (HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E BINAND))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE AND))
(CALL 2. (E XCONS))
TAG5
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP BINOR SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (OR FALSE FALSE)))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE FALSE))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG3 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG4)
(MOVE 2. 0. P)
(MOVEI 1. (QUOTE OR))
(CALL 2. (E CONS))
(JRST 0. TAG1)
TAG4 (HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E BINOR))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
TAG5
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP BYPART SUBR)
(CALL 1. (E GETLINE))
(JCALL 1. (E CADDR))
NIL
(LAP BOUNDSUBST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E ATOM))
(JUMPN 1. TAG1)
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPN 1. TAG2)
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 3. (E BOUNDSUBSTL))
(JRST 0. TAG3)
TAG1 (MOVE 1. -3. P)
(CALL 1. (E ISCONST))
(JUMPE 1. TAG9)
(MOVE 1. -3. P)
(JRST 0. TAG3)
TAG9 (MOVE 2. -1. P)
(MOVE 1. -3. P)
(CALL 2. (E ASSOC))
(MOVEM 1. 0. P)
(JUMPE 1. TAG11)
(HRRZ@ 1. 1.)
(JRST 0. TAG3)
TAG11 (MOVE 2. -1. P)
(MOVE 1. -3. P)
(CALL 2. (E ASSOCR))
(MOVEM 1. 0. P)
(JUMPE 1. TAG13)
(MOVEI 1. (QUOTE (FREE VARIABLE CAPTURE)))
(CALL 1. (E ERREND))
TAG13 (MOVE 1. -3. P)
(JRST 0. TAG3)
TAG2 (MOVE 2. -2. P)
(HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
(CALL 2. (E ASSOC))
(MOVEM 1. 0. P)
(JUMPE 1. TAG15)
(HRRZ@ 1. 1.)
(JRST 0. TAG14)
TAG15 (HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
TAG16
TAG14 (MOVEM 1. 0. P)
(MOVE 2. -1. P)
(CALL 2. (E ASSOCR))
(JUMPE 1. TAG19)
(MOVEI 1. (QUOTE (BOUND VARIABLE CAPTURE)))
(CALL 1. (E ERREND))
TAG19 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(HLRZ@ 2. -3. P)
(HLRZ@ 2. 2.)
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(MOVE 2. -2. P)
(CALL 2. (E CONS))
(MOVE 3. 1.)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 3. (E BOUNDSUBST))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
TAG3 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP BOUNDSUBSTL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPE 1. TAG1)
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 3. (E BOUNDSUBST))
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(CALL 3. (E BOUNDSUBSTL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG2
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP CONJOIN SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE TRUE))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG3)
(HLRZ@ 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE AND))
(CALL 2. (E CONS))
TAG4
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP CURCOL SUBR)
(MOVEI 1. (QUOTE NIL))
(CALL 1. (E LINELENGTH))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE 1.))
(CALL 2. (E *DIF))
(POP P 2.)
(JCALL 2. (E *PLUS))
NIL
(LAP CURLINE SUBR)
(CALL 0. (E CURPROOF))
(MOVE 1. (SPECIAL CURLIN))
(POPJ P)
NIL
(LAP CURPROOF SUBR)
(MOVE 1. (SPECIAL CURPRF))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (NO CURRENT PROOF)))
(CALL 1. (E ERREND))
(JRST 0. TAG1)
TAG2 (MOVE 1. (SPECIAL CURPRF))
TAG3
TAG1 (POPJ P)
NIL
(LAP CURTEXT SUBR)
(CALL 0. (E CURPROOF))
(MOVEI 2. (QUOTE PROOF))
(JCALL 2. (E GET))
NIL
(LAP DOUBLENEG SUBR)
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (NOT (NOT PPP))))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE PPP))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
TAG3
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP EXGEN1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
TAG1 (MOVE 1. 0. P)
(JUMPN 1. TAG9)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG9 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (ILLEGAL ARGUMENT)))
(CALL 1. (E ERREND))
TAG2 (HLRZ@ 3. 0. P)
(HLRZ@ 2. 0. P)
(MOVE 1. -1. P)
(CALL 3. (E EXGEN))
(MOVEM 1. -1. P)
(JRST 0. TAG4)
TAG3 (HLRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(MOVE 1. -1. P)
(CALL 3. (E EXGEN))
(MOVEM 1. -1. P)
TAG4 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG5 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EXGEN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 0. (E GENSYM))
(MOVE 3. -2. P)
(MOVE 2. -1. P)
(PUSH P 1.)
(CALL 3. (E SUBST))
(MOVEM 1. -3. P)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE (NEW VARIABLE CONFLICTS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. -1. P)
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE THEREEXISTS))
(CALL 2. (E XCONS))
(MOVE 3. -3. P)
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 3. (E SUBST))
(CALL 1. (E NCONS))
(POP P 2.)
(SUB P (C 0. 0. 4. 4.))
(JCALL 2. (E XCONS))
NIL
(LAP EQI1 SUBR)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES QQQ PPP)))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE (EQUIVALENT PPP QQQ)))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
TAG3
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ERREND SUBR)
(PUSH P 1.)
(CALL 1. (E PRINT))
(CALL 0. (E ERR))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP FREEIN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(MOVE 1. 2.)
(JUMPE 1. TAG1)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E FREEVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG2)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (HRRZ@ 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E FREEIN))
TAG3
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP FREEVARS SUBR)
(MOVE 3. 1.)
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE NIL))
(JCALL 3. (E FREEVARS1))
NIL
(LAP FREEVARS1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 3.)
(CALL 1. (E ISVAR))
(JUMPE 1. TAG4)
(MOVE 2. -2. P)
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG6)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG6 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG7)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG7 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E CONS))
TAG8
TAG5 (JRST 0. TAG3)
TAG4 (MOVE 1. -1. P)
TAG10
TAG3 (JRST 0. TAG1)
TAG2 (HLRZ@ 1. 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG12)
(HRRZ@ 3. 3.)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS2))
(JRST 0. TAG1)
TAG12 (HLRZ@ 1. 3.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG13)
(MOVEI 2. (QUOTE (FORALL THEREEXISTS)))
(HLRZ@ 1. 3.)
(HLRZ@ 1. 1.)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG15)
(MOVE 2. -2. P)
(HLRZ@ 1. 0. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(HRRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(MOVE 2. -1. P)
(CALL 3. (E FREEVARS1))
TAG15 (JRST 0. TAG1)
TAG13 (MOVEI 1. (QUOTE (UNKNOWN NONATOMIC FUNCTION)))
(CALL 1. (E ERREND))
TAG16
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP FREEVARS2 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPN 3. TAG2)
(MOVE 1. 2.)
(JRST 0. TAG1)
TAG2 (HRRZ@ 3. 0. P)
(MOVE 2. -1. P)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS2))
(HLRZ@ 3. 0. P)
(MOVE 2. 1.)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS1))
TAG3
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP GETCURLINE SUBR)
(CALL 0. (E CURLINE))
(JCALL 1. (E GETLINE))
NIL
(LAP GETLINE SUBR)
(PUSH P 1.)
(CALL 0. (E CURTEXT))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E ASSOC))
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH LINE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. 0. P)
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP GIVEPROOF FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC PROOF NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL PROOFS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL PROOFS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL PROOFS))
TAG7 (MOVEI 3. (QUOTE PROOF))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP IFE1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -2. P)
(EXCH 1. -3. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVEM 1. -2. P)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE RRR))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVE 1. -3. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG4)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -3. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG4 (MOVE 1. -2. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG5)
(MOVEI 2. (QUOTE RRR))
(MOVE 1. -2. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG5 (MOVEI 1. (QUOTE INVALID))
TAG6
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP IFI1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR)))
(CALL 3. (E INST))
(POP P 2.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR)))
(CALL 3. (E INST))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE (COND (PPP QQQ) (T RRR))))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE (COND (PPP QQQ) (T RRR))))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE INVALID))
TAG4
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP INITALL SUBR)
(CLEARM 1. (SPECIAL CURPRF))
(CLEARM 1. (SPECIAL AXIOMS))
(CLEARM 1. (SPECIAL THEOREMS))
(CLEARM 1. (SPECIAL PROOFS))
(CLEARM 1. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INITOPS SUBR)
(MOVE 2. (SPECIAL PRECLIS*))
(MOVEI 1. (QUOTE SETQ))
(CALL 2. (E CONS))
(MOVEI 2. (QUOTE *COMMA*))
(CALL 2. (E XCONS))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPE 1. TAG3)
(HLRZ@ 1. 1.)
(MOVEI 2. (QUOTE INFIX))
(MOVEM 1. -1. P)
(CALL 2. (E GET))
(MOVEM 1. -2. P)
(MOVEI 2. (QUOTE LEFT))
(MOVE 1. -1. P)
(CALL 2. (E GET))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE 1.))
(CALL 1. (E MINUS))
(JRST 0. TAG6)
TAG7 (MOVEI 1. (QUOTE 1.))
TAG8
TAG6 (MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE 3.))
(CALL 2. (E *TIMES))
(MOVE 2. 0. P)
(CALL 2. (E *PLUS))
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE 3.))
(CALL 2. (E *TIMES))
(MOVE 2. -1. P)
(CALL 2. (E *DIF))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 3. (QUOTE PREC))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 3. (E PUTPROP))
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INITPROOF SUBR)
(PUSH P 1.)
(JUMPN 1. TAG6)
(MOVEI 1. (QUOTE (NIL NOT ACCEPTABLE PROOF NAME)))
(CALL 1. (E ERREND))
TAG6 (MOVE 1. 0. P)
(MOVEM 1. (SPECIAL CURPRF))
(MOVEI 2. (QUOTE (PROOF)))
(MOVE 1. 0. P)
(CALL 2. (E GETL))
(JUMPN 1. TAG1)
(MOVEI 3. (QUOTE PROOF))
(MOVEI 2. (QUOTE NIL))
(MOVE 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL PROOFS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL PROOFS))
TAG1 (CALL 0. (E CURTEXT))
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE 0.))
(JRST 0. TAG8)
TAG9 (CALL 0. (E CURTEXT))
(CALL 1. (E LAST))
(CALL 1. (E CAAR))
TAG10
TAG8 (MOVEM 1. (SPECIAL CURLIN))
(CALL 0. (E CURLINE))
(MOVEI 3. (QUOTE NEWNAM))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE /@))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INITSTANCHARSET SUBR)
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∧))
(MOVEI 1. (QUOTE AND))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE →→))
(MOVEI 1. (QUOTE CMAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /,))
(MOVEI 1. (QUOTE *COMMA*))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /.))
(MOVEI 1. (QUOTE CONS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊂))
(MOVEI 1. (QUOTE CONTAINED))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE DIFFERENCE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =))
(MOVEI 1. (QUOTE EQUAL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≡))
(MOVEI 1. (QUOTE EQUIVALENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ↑))
(MOVEI 1. (QUOTE EXPT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∀))
(MOVEI 1. (QUOTE FORALL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≥))
(MOVEI 1. (QUOTE GEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >))
(MOVEI 1. (QUOTE GREATERP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊃))
(MOVEI 1. (QUOTE IMPLIES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∩))
(MOVEI 1. (QUOTE INTERSECTION))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE λ))
(MOVEI 1. (QUOTE LAMBDA))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≤))
(MOVEI 1. (QUOTE LEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <))
(MOVEI 1. (QUOTE LESSP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE →))
(MOVEI 1. (QUOTE MAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ε))
(MOVEI 1. (QUOTE MEMBER))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE MINUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≠))
(MOVEI 1. (QUOTE NEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ¬))
(MOVEI 1. (QUOTE NOT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∨))
(MOVEI 1. (QUOTE OR))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /+))
(MOVEI 1. (QUOTE PLUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊗))
(MOVEI 1. (QUOTE PRODUCT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE '))
(MOVEI 1. (QUOTE QUOTE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE //))
(MOVEI 1. (QUOTE QUOTIENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ←))
(MOVEI 1. (QUOTE SETQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∃))
(MOVEI 1. (QUOTE THEREEXISTS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE *))
(MOVEI 1. (QUOTE TIMES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∪))
(MOVEI 1. (QUOTE UNION))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INITTTYCHARSET SUBR)
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE &))
(MOVEI 1. (QUOTE AND))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / CMAPS/ ))
(MOVEI 1. (QUOTE CMAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /,))
(MOVEI 1. (QUOTE *COMMA*))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /.))
(MOVEI 1. (QUOTE CONS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / CONT/ ))
(MOVEI 1. (QUOTE CONTAINED))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE DIFFERENCE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =))
(MOVEI 1. (QUOTE EQUAL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <=>))
(MOVEI 1. (QUOTE EQUIVALENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ↑))
(MOVEI 1. (QUOTE EXPT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE A))
(MOVEI 1. (QUOTE FORALL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >=))
(MOVEI 1. (QUOTE GEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >))
(MOVEI 1. (QUOTE GREATERP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =>))
(MOVEI 1. (QUOTE IMPLIES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / INTERSECT/ ))
(MOVEI 1. (QUOTE INTERSECTION))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE L))
(MOVEI 1. (QUOTE LAMBDA))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <=))
(MOVEI 1. (QUOTE LEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <))
(MOVEI 1. (QUOTE LESSP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / MAPS/ ))
(MOVEI 1. (QUOTE MAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / MEMBER/ ))
(MOVEI 1. (QUOTE MEMBER))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE MINUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / NEQ/ ))
(MOVEI 1. (QUOTE NEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE NOT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / V/ ))
(MOVEI 1. (QUOTE OR))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /+))
(MOVEI 1. (QUOTE PLUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / PROD/ ))
(MOVEI 1. (QUOTE PRODUCT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE '))
(MOVEI 1. (QUOTE QUOTE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE //))
(MOVEI 1. (QUOTE QUOTIENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ←))
(MOVEI 1. (QUOTE SETQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE E))
(MOVEI 1. (QUOTE THEREEXISTS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE *))
(MOVEI 1. (QUOTE TIMES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / UNION/ ))
(MOVEI 1. (QUOTE UNION))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 3.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVE 1. -1. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE (PPP QQQ RRR SSS)))
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG5)
(MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E ASSOC))
(PUSH P 1.)
(JUMPN 1. TAG7)
(MOVE 2. -3. P)
(MOVE 1. -2. P)
(CALL 2. (E CONS))
(MOVE 2. -1. P)
(CALL 2. (E CONS))
(JRST 0. TAG6)
TAG7 (MOVE 2. -3. P)
(HRRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG8)
(MOVE 1. -1. P)
(JRST 0. TAG6)
TAG8 (MOVEI 1. (QUOTE INVALID))
TAG9
TAG6 (SUB P (C 0. 0. 1. 1.))
(JRST 0. TAG4)
TAG5 (MOVE 1. -1. P)
(CAME 1. -2. P)
(JRST 0. TAG11)
(MOVE 1. 0. P)
(JRST 0. TAG4)
TAG11 (MOVEI 1. (QUOTE INVALID))
TAG12
TAG4 (JRST 0. TAG1)
TAG3 (MOVE 1. -2. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG14)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG14 (HRRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(MOVE 3. -1. P)
(HLRZ@ 2. -2. P)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 3. (E INST))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E INST))
(SUB P (C 0. 0. 1. 1.))
TAG15
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP ISCONST SUBR)
(PUSH P 1.)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG1)
(MOVE 2. (SPECIAL LOGICALCONSTANTS))
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG1)
(TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ISEQUIVALENCE SUBR)
(MOVEI 2. (QUOTE (EQUAL EQUIVALENT SETQ)))
(JCALL 2. (E MEMBER))
NIL
(LAP ISIDENT SUBR)
(PUSH P 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG1)
TAG2 (TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ISQUANT SUBR)
(MOVE 2. (SPECIAL QUANTIFIERS))
(JCALL 2. (E MEMBER))
NIL
(LAP ISVAR SUBR)
(PUSH P 1.)
(CALL 1. (E ISIDENT))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(CALL 1. (E ISCONST))
(JUMPE 1. TAG1)
TAG2 (TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP LAMEXP SUBR)
(PUSH P 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG3)
(HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E LAMEXPL))
(POP P 2.)
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG3 (MOVEI 2. (QUOTE LAMBDA))
(HLRZ@ 1. 0. P)
(CALL 1. (E CAAR))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG4)
(HLRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 3. (E PROPSUBST))
(JRST 0. TAG1)
TAG4 (HLRZ@ 1. 0. P)
(CALL 1. (E LAMEXP))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E LAMEXPL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG5
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP LAMEXPL SUBR)
(MOVE 2. 1.)
(MOVEI 1. (QUOTE LAMEXP))
(JCALL 2. (E MAPCAR))
NIL
(LAP MAKECONSES SUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -1. P)
(JUMPN 1. TAG6)
(MOVE 1. 0. P)
(JRST 0. TAG2)
TAG6 (HLRZ@ 1. -1. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG9)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPN 1. TAG9)
(HLRZ@ 1. -1. P)
(CALL 1. (E LENGTH))
(MOVEI 2. (QUOTE 3.))
(CALL 2. (E NEQ))
(JUMPE 1. TAG8)
TAG9 (MOVEI 1. (QUOTE (BAD ARGUMENT)))
(CALL 1. (E ERREND))
TAG8 (HLRZ@ 2. -1. P)
(HRRZ@ 2. 2.)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. -1. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(MOVE 2. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
(HRRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP MAKERNL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -6. P)
(JUMPN 1. TAG10)
(MOVE 1. -3. P)
(JRST 0. TAG6)
TAG10 (HLRZ@ 1. -6. P)
(MOVEM 1. -4. P)
(MOVE 2. -5. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
TAG2 (HRRZ@ 1. -6. P)
(MOVEM 1. -6. P)
(JRST 0. TAG1)
TAG3 (MOVE 1. -4. P)
(CALL 1. (E ALPHAPART))
(MOVEM 1. -1. P)
(MOVEI 1. (QUOTE 1.))
(MOVEM 1. 0. P)
TAG4 (MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E MAKESYM))
(MOVEM 1. -2. P)
(MOVE 2. -5. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG5)
(MOVE 2. -2. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 2. -3. P)
(CALL 2. (E CONS))
(MOVEM 1. -3. P)
(JRST 0. TAG2)
TAG5 (MOVEI 2. (QUOTE 1.))
(MOVE 1. 0. P)
(CALL 2. (E *PLUS))
(MOVEM 1. 0. P)
(JRST 0. TAG4)
TAG6 (SUB P (C 0. 0. 7. 7.))
(POPJ P)
NIL
(LAP MAKEVAR SUBR)
(PUSH P 1.)
(PUSH P 2.)
(CALL 1. (E NCONS))
(MOVE 2. 0. P)
(CALL 2. (E MAKERNL))
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVE 1. -2. P)
(JRST 0. TAG4)
TAG5 (HLRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
TAG6
TAG4 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP MAKESYM SUBR)
(PUSH P 2.)
(CALL 1. (E EXPLODE))
(EXCH 1. 0. P)
(CALL 1. (E EXPLODE))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E *APPEND))
(JCALL 1. (E READLIST))
NIL
(LAP MAKETHEOREM1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 3.)
(CALL 1. (E INITPROOF))
(MOVE 1. -1. P)
(CALL 1. (E ASSPART))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE (STILL HAS ASSUMPTIONS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. -1. P)
(CALL 1. (E WFFPART))
(MOVEI 3. (QUOTE THEOREM))
(MOVE 2. 1.)
(MOVE 1. -2. P)
(CALL 3. (E PUTPROP))
(MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(MOVEI 3. (QUOTE BY))
(MOVE 2. 1.)
(MOVE 1. -2. P)
(CALL 3. (E PUTPROP))
(MOVE 1. -2. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL THEOREMS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL THEOREMS))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG7)
(MOVE 1. -2. P)
(CALL 1. (E SHOWTHEOREM))
TAG7 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP MP1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP IMPLIES PPP QQQ)))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVE 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP IMPLIES PPP QQQ)))
(CALL 3. (E INST))
(MOVEM 1. 0. P)
TAG5 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG7)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG7 (MOVEI 2. (QUOTE QQQ))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG8 (MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP NEXTLINE SUBR)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(JCALL 2. (E *PLUS))
NIL
(LAP NOTELIM SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP NOT PPP)))
(CALL 3. (E INST))
(POP P 2.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP NOT PPP)))
(CALL 3. (E INST))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVE 1. 0. P)
(JRST 0. TAG1)
TAG2 (MOVE 1. -1. P)
TAG3
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP NOTINTRO SUBR)
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (IMPLIES PPP FALSE)))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE (NOT PPP)))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
TAG3
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP NTHCDR SUBR)
(PUSH P 1.)
(PUSH P 2.)
(MOVEI 2. (QUOTE 0.))
(MOVE 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG2)
(MOVE 1. -1. P)
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. -1. P)
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E NTHCDR))
TAG3
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP NTHELT SUBR)
(PUSH P 2.)
(MOVEI 2. (QUOTE 1.))
(EXCH 1. 0. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E NTHCDR))
(HLRZ@ 1. 1.)
(POPJ P)
NIL
(LAP NUMPART SUBR)
(CALL 1. (E GETLINE))
(HLRZ@ 1. 1.)
(POPJ P)
NIL
(LAP ORELIM1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVEI 2. (QUOTE OR))
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE (FIRST ARG MUST BE DISJUNCTION)))
(CALL 1. (E ERREND))
TAG7 (HRRZ@ 1. -4. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO DISJUNCTS)))
(CALL 1. (E ERREND))
TAG9 (MOVE 1. -3. P)
(JUMPN 1. TAG11)
(MOVEI 1. (QUOTE (NEED AT LEAST ONE IMPLICATION)))
(CALL 1. (E ERREND))
TAG11 (HRRZ@ 1. -4. P)
(MOVEM 1. -1. P)
(HLRZ@ 1. -3. P)
(CALL 1. (E CDDR))
(MOVEM 1. -2. P)
TAG1 (MOVEI 2. (QUOTE IMPLIES))
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPE 1. TAG13)
(MOVEI 1. (QUOTE (ARG NOT IMPLICATION)))
(CALL 1. (E ERREND))
TAG13 (MOVE 2. -2. P)
(HLRZ@ 1. -3. P)
(CALL 1. (E CDDR))
(CALL 2. (E NEQ))
(JUMPE 1. TAG15)
(MOVEI 1. (QUOTE (MULTIPLE CONCLUSIONS)))
(CALL 1. (E ERREND))
TAG15 (MOVE 2. 0. P)
(HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JUMPN 1. TAG1)
TAG2 (MOVE 1. -1. P)
(JUMPN 1. TAG18)
(HLRZ@ 1. -2. P)
(JRST 0. TAG3)
TAG18 (MOVE 2. 0. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG20)
(MOVEI 1. (QUOTE (UNPROVEN DISJUNCT)))
(CALL 1. (E ERREND))
TAG20 (HRRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(JRST 0. TAG2)
TAG3 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP PCERR SUBR)
(MOVEI 1. (QUOTE PROOF/ CHECKER))
(CALL 1. (E PRINC))
(MOVE 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(CLEARM 1. (SPECIAL *FILEPRINT))
(MOVEI 1. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(MOVEM 1. (SPECIAL *PRINT))
(MOVEI 1. (QUOTE NIL))
(CLEARM 1. (SPECIAL *TWODIM))
(MOVEI 1. (QUOTE NIL))
(MOVEI 1. (QUOTE (BEGIN)))
(CALL 1. (E *EVAL))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP PCINIT SUBR)
(CALL 0. (E EXCISE))
(CALL 0. (E ONDD))
(CALL 0. (E INITOPS))
(CALL 0. (E INITALL))
(MOVEI 1. (QUOTE PCSTART))
(CALL 1. (E INITFN))
(MOVEI 1. (QUOTE PROOF/ CHECKER/ INITIALIZED))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP SUBFUN1PCSTART SUBR)
(MOVEI 1. (QUOTE ((CONS PCHECK INI))))
(JCALL 15. (E RESTOREALL))
NIL
(LAP PCSTART SUBR)
(MOVEI 1. (QUOTE ((SUBFUN1PCSTART) NIL)))
(CALL 15. (E ERRSET))
(MOVEI 1. (QUOTE PCERR))
(CALL 1. (E INITFN))
(CALL 0. (E PCERR))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP PAIRLIS SUBR)
(PUSH P 1.)
(PUSH P 2.)
(JUMPE 1. TAG3)
(JUMPN 2. TAG2)
TAG3 (MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG2 (HLRZ@ 2. 0. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E CONS))
(HRRZ@ 2. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(CALL 2. (E PAIRLIS))
(POP P 2.)
(CALL 2. (E XCONS))
TAG4
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP PROPSUBST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 1. (E FREEVARS))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E MAKERNL))
(MOVE 4. 1.)
(POP P 3.)
(POP P 2.)
(POP P 1.)
(JCALL 4. (E PROPSUBST1))
NIL
(LAP PROPSUBST1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(MOVE 1. 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 3.)
(CALL 1. (E ISVAR))
(JUMPE 1. TAG4)
(MOVE 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG6)
(MOVE 1. -3. P)
(JRST 0. TAG5)
TAG6 (MOVE 1. -1. P)
TAG7
TAG5 (JRST 0. TAG3)
TAG4 (MOVE 1. -1. P)
TAG9
TAG3 (JRST 0. TAG1)
TAG2 (HLRZ@ 1. 3.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG11)
(HLRZ@ 1. 3.)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPE 1. TAG11)
(MOVE 2. -2. P)
(HLRZ@ 1. -1. P)
(CALL 1. (E CADR))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG14)
(MOVE 1. -1. P)
(JRST 0. TAG13)
TAG14 (MOVE 2. 0. P)
(HLRZ@ 1. -1. P)
(CALL 1. (E CADR))
(CALL 2. (E ASSOC))
(PUSH P 1.)
(JUMPN 1. TAG21)
(HLRZ@ 1. -2. P)
(CALL 1. (E CADR))
(JRST 0. TAG20)
TAG21 (HRRZ@ 1. 0. P)
TAG22
TAG20 (MOVEM 1. 0. P)
(CALL 1. (E NCONS))
(HLRZ@ 2. -2. P)
(HLRZ@ 2. 2.)
(CALL 2. (E XCONS))
(HRRZ@ 3. -2. P)
(HLRZ@ 3. 3.)
(HLRZ@ 2. -2. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 3. (E SUBST))
(MOVE 4. -2. P)
(MOVE 3. 1.)
(MOVE 2. -4. P)
(MOVE 1. -5. P)
(CALL 4. (E PROPSUBST1))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(SUB P (C 0. 0. 1. 1.))
TAG15
TAG13 (JRST 0. TAG1)
TAG11 (MOVE 4. 0. P)
(HLRZ@ 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 4. (E PROPSUBST1))
(MOVE 4. 0. P)
(HRRZ@ 3. -1. P)
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVE 1. -4. P)
(CALL 4. (E PROPSUBSTL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG24
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP PROPSUBSTL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(MOVE 1. 3.)
(JUMPE 1. TAG1)
(MOVE 4. 0. P)
(HLRZ@ 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 4. (E PROPSUBST1))
(MOVE 4. 0. P)
(HRRZ@ 3. -1. P)
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVE 1. -4. P)
(CALL 4. (E PROPSUBSTL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG2
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP QUANTEQUIV SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVE 1. 3.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG6)
(HLRZ@ 1. -5. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG3)
(HLRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPN 1. TAG4)
TAG1 (MOVE 1. -5. P)
(JUMPN 1. TAG13)
(MOVE 1. -3. P)
(JUMPE 1. TAG14)
(TDZA 1. 1.)
TAG14 (MOVEI 1. (QUOTE T))
(JRST 0. TAG5)
TAG13 (MOVE 4. -2. P)
(HLRZ@ 3. -3. P)
(MOVE 2. -4. P)
(HLRZ@ 1. -5. P)
(CALL 4. (E QUANTEQUIV))
(JUMPE 1. TAG6)
(HRRZ@ 1. -5. P)
(MOVEM 1. -5. P)
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG2 (MOVE 2. -4. P)
(MOVE 1. -5. P)
(CALL 2. (E ASSOC))
(MOVEM 1. -1. P)
(JUMPE 1. TAG17)
(CALL 1. (E CDAR))
(MOVEM 1. -5. P)
TAG17 (MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 2. (E ASSOC))
(MOVEM 1. -1. P)
(JUMPE 1. TAG19)
(CALL 1. (E CDAR))
(MOVEM 1. -5. P)
TAG19 (MOVE 2. -3. P)
(MOVE 1. -5. P)
(CALL 2. (E EQUAL))
(JRST 0. TAG5)
TAG3 (HLRZ@ 2. -3. P)
(HLRZ@ 1. -5. P)
(CALL 2. (E NEQ))
(JUMPN 1. TAG6)
(HRRZ@ 1. -5. P)
(MOVEM 1. -5. P)
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG4 (HLRZ@ 1. -3. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG6)
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPE 1. TAG6)
(HLRZ@ 2. -3. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPN 1. TAG6)
(CALL 0. (E GENSYM))
(HLRZ@ 2. -5. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(MOVEM 1. 0. P)
(CALL 2. (E XCONS))
(MOVE 2. -4. P)
(CALL 2. (E CONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(MOVE 2. -3. P)
(CALL 2. (E CONS))
(MOVE 4. 1.)
(HRRZ@ 3. -4. P)
(HLRZ@ 3. 3.)
(POP P 2.)
(HRRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 4. (E QUANTEQUIV))
(JRST 0. TAG5)
TAG6 (MOVEI 1. (QUOTE NIL))
TAG5 (SUB P (C 0. 0. 6. 6.))
(POPJ P)
NIL
(LAP REPEITHER SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(HLRZ@ 1. 2.)
(CALL 1. (E ISEQUIVALENCE))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (NO EQUATION)))
(CALL 1. (E ERREND))
(JRST 0. TAG1)
TAG2 (MOVE 1. -1. P)
(JUMPE 1. TAG6)
(HRRZ@ 1. -2. P)
(CALL 1. (E CADR))
(JRST 0. TAG5)
TAG6 (HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
TAG7
TAG5 (PUSH P 1.)
(MOVE 2. -2. P)
(JUMPE 2. TAG10)
(HRRZ@ 2. -3. P)
(HLRZ@ 2. 2.)
(JRST 0. TAG9)
TAG10 (HRRZ@ 2. -3. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
TAG11
TAG9 (MOVE 4. -1. P)
(MOVE 3. -4. P)
(POP P 1.)
(CALL 4. (E REPNTH))
TAG3
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP REPNTH SUBR)
(JSP 6. SPECBIND)
(0. 0. (SPECIAL ORDCNT))
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(MOVEI 1. (QUOTE 0.))
(MOVEM 1. (SPECIAL ORDCNT))
(MOVE 5. 4.)
(MOVEI 4. (QUOTE NIL))
(MOVE 1. -3. P)
(CALL 5. (E REPNTH1))
(PUSH P 1.)
(MOVE 2. -1. P)
(MOVE 1. (SPECIAL ORDCNT))
(CALL 2. (E *LESS))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE (NO REPLACEMENT)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. 0. P)
(SUB P (C 0. 0. 5. 5.))
(JRST 0. SPECSTR)
NIL
(LAP REPNTH1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVEI 2. (QUOTE NIL))
(MOVE 1. -6. P)
(CALL 4. (E QUANTEQUIV))
(JUMPN 1. TAG2)
(MOVE 1. -5. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG8)
(MOVE 1. -5. P)
(JRST 0. TAG3)
TAG8 (HLRZ@ 1. -5. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG10)
(HLRZ@ 1. -5. P)
(MOVE 5. -3. P)
(MOVE 4. -4. P)
(HRRZ@ 3. -5. P)
(MOVE 2. -6. P)
(PUSH P 1.)
(MOVE 1. -8. P)
(CALL 5. (E REPNTHL))
(POP P 2.)
(CALL 2. (E XCONS))
(JRST 0. TAG3)
TAG10 (HLRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPN 1. TAG1)
TAG1 (CALL 0. (E GENSYM))
(MOVEM 1. -1. P)
(HLRZ@ 1. -5. P)
(CALL 1. (E CADR))
(MOVEM 1. 0. P)
(MOVE 1. -7. P)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG13)
(HRRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E MAKEVAR))
(JRST 0. TAG12)
TAG13 (MOVE 1. 0. P)
TAG14
TAG12 (MOVEM 1. -2. P)
(CALL 1. (E NCONS))
(HLRZ@ 2. -5. P)
(HLRZ@ 2. 2.)
(CALL 2. (E XCONS))
(HRRZ@ 3. -5. P)
(HLRZ@ 3. 3.)
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 3. (E SUBST))
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 2. -6. P)
(CALL 2. (E CONS))
(MOVE 5. -5. P)
(MOVE 4. 1.)
(POP P 3.)
(MOVE 2. -7. P)
(MOVE 1. -8. P)
(CALL 5. (E REPNTH1))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(JRST 0. TAG3)
TAG2 (MOVEI 2. (QUOTE 1.))
(MOVE 1. (SPECIAL ORDCNT))
(CALL 2. (E *PLUS))
(MOVEM 1. (SPECIAL ORDCNT))
(MOVE 2. -3. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG17)
(MOVE 1. -7. P)
(JRST 0. TAG16)
TAG17 (MOVE 1. -5. P)
TAG18
TAG16
TAG3 (SUB P (C 0. 0. 8. 8.))
(POPJ P)
NIL
(LAP REPNTHL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(MOVE 1. 3.)
(JUMPE 1. TAG1)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(HLRZ@ 3. -2. P)
(MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 5. (E REPNTH1))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(HRRZ@ 3. -2. P)
(MOVE 2. -3. P)
(PUSH P 1.)
(MOVE 1. -5. P)
(CALL 5. (E REPNTHL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG2
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP SAVEAXIOM SUBR)
(MOVEI 2. (QUOTE AXIOM))
(PUSH P 1.)
(CALL 2. (E GET))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE ADDAXIOM))
(CALL 2. (E XCONS))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVEAXCOM SUBR)
(MOVEI 2. (QUOTE AXIOM))
(PUSH P 1.)
(CALL 2. (E GET))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE GIVEAX))
(CALL 2. (E XCONS))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVEPRFCOM SUBR)
(PUSH P 1.)
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE PROOF))
(CALL 2. (E XCONS))
(CALL 1. (E PRINT))
(MOVEI 2. (QUOTE PROOF))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(PUSH P 1.)
TAG1 (MOVE 1. 0. P)
(JUMPN 1. TAG6)
(CALL 0. (E TERPRI))
(JRST 0. TAG2)
TAG6 (HLRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(MOVEI 2. (QUOTE USETHM))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG8)
(HLRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(CALL 1. (E CADR))
(CALL 1. (E SAVETHMCOM))
TAG8 (HLRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 1. (E PRINT))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(HLRZ@ 1. 0. P)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 9.))
(CALL 1. (E CADDR))
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP SAVEPROOF SUBR)
(MOVEI 2. (QUOTE PROOF))
(PUSH P 1.)
(CALL 2. (E GET))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE GIVEPROOF))
(CALL 2. (E XCONS))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVESCHEMA SUBR)
(MOVEI 2. (QUOTE SCHEMA))
(PUSH P 1.)
(CALL 2. (E GET))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE ADDSCHEMA))
(CALL 2. (E XCONS))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVESCHMCOM SUBR)
(MOVEI 2. (QUOTE SCHEMA))
(PUSH P 1.)
(CALL 2. (E GET))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE GIVESCHM))
(CALL 2. (E XCONS))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVETHEOREM SUBR)
(MOVEI 2. (QUOTE BY))
(PUSH P 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E GET))
(CALL 1. (E CADR))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE ADDTHM))
(CALL 2. (E XCONS))
(SUB P (C 0. 0. 2. 2.))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SAVETHMCOM SUBR)
(MOVEI 2. (QUOTE BY))
(PUSH P 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E GET))
(CALL 1. (E CADR))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE MAKETHM))
(CALL 2. (E XCONS))
(SUB P (C 0. 0. 2. 2.))
(JCALL 1. (E PRINTEXPR))
NIL
(LAP SETDIF SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG6)
(MOVE 1. 0. P)
(CALL 1. (E REVERSE))
(JRST 0. TAG2)
TAG6 (MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG8)
(MOVE 2. 0. P)
(HLRZ@ 1. -2. P)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG8 (HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SHOWAXIOM SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE AXIOM))
(CALL 1. (E PRINT))
(MOVE 1. 0. P)
(CALL 1. (E PRINC))
(CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE AXIOM))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(CALL 1. (E SHOWEXP))
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP SHOWCURLINE SUBR)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 0.))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG2)
(MOVEI 1. (QUOTE NIL))
(CALL 15. (E SHOW))
(JRST 0. TAG1)
TAG2 (CALL 0. (E GETCURLINE))
(CALL 1. (E SHOWLINE))
TAG3
TAG1 (POPJ P)
NIL
(LAP SHOWEXP SUBR)
(PUSH P 1.)
(MOVE 1. (SPECIAL *TWODIM))
(JUMPE 1. TAG2)
(CALL 0. (E CURCOL))
(MOVEI 3. (QUOTE 0.))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E TDDEXP))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E INFX))
TAG3
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP SHOWLINE SUBR)
(PUSH P 1.)
(CALL 0. (E TERPRI))
(CALL 0. (E TERPRI))
(HLRZ@ 1. 0. P)
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE :))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 1. (E SHOWEXP))
(MOVEI 1. (QUOTE BY))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(PUSH P 1.)
(MOVEI 2. (QUOTE ASS))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG1)
(MOVEI 2. (QUOTE USEAX))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(HRRZ@ 2. 0. P)
(MOVEI 1. (QUOTE AXIOM))
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG7 (MOVEI 2. (QUOTE USESCHM))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG9)
(HRRZ@ 2. 0. P)
(MOVEI 1. (QUOTE SCHEMA))
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG9 (MOVEI 2. (QUOTE USETHM))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG11)
(HRRZ@ 2. 0. P)
(MOVEI 1. (QUOTE THEOREM))
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG11 (MOVE 1. 0. P)
(CALL 1. (E SHOWEXP))
(HRRZ@ 1. -1. P)
(CALL 1. (E CADDR))
(JUMPE 1. TAG3)
(MOVEI 1. (QUOTE ASSUMING))
(CALL 1. (E PRINS))
(HRRZ@ 1. -1. P)
(CALL 1. (E CADDR))
(CALL 1. (E PRINS))
(JRST 0. TAG3)
TAG1 (MOVEI 1. (QUOTE ASSUMPTION))
(CALL 1. (E PRINS))
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP SHOWPROOF SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE PROOF))
(CALL 1. (E PRINT))
(MOVE 1. 0. P)
(CALL 1. (E PRINS))
(MOVEI 2. (QUOTE PROOF))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(EXCH 2. 1.)
(MOVEI 1. (QUOTE SHOWLINE))
(CALL 2. (E MAPC))
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP SHOWSCHEMA SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE SCHEMA))
(CALL 1. (E PRINT))
(MOVE 1. 0. P)
(CALL 1. (E PRINC))
(CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE SCHEMA))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(CALL 1. (E SHOWEXP))
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP SHOWTHEOREM SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE THEOREM))
(CALL 1. (E PRINT))
(MOVE 1. 0. P)
(CALL 1. (E PRINS))
(CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE THEOREM))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(CALL 1. (E SHOWEXP))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(DEFPROP AXIOM SHOWAXIOM IMAGE)
(DEFPROP PROOF SHOWPROOF IMAGE)
(DEFPROP SCHEMA SHOWSCHEMA IMAGE)
(DEFPROP THEOREM SHOWTHEOREM IMAGE)
(LAP SPECALL SUBR)
(PUSH P 1.)
(PUSH P 2.)
TAG1 (MOVE 1. 0. P)
(JUMPN 1. TAG6)
(MOVE 1. -1. P)
(JRST 0. TAG2)
TAG6 (MOVE 1. -1. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG8)
(MOVEI 1. (QUOTE (ATOMIC EXPRESSION)))
(CALL 1. (E ERREND))
TAG8 (MOVEI 2. (QUOTE FORALL))
(HLRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPE 1. TAG10)
(MOVEI 2. (QUOTE THEREEXISTS))
(HLRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E NEQ))
(JUMPE 1. TAG10)
(MOVEI 1. (QUOTE (NOT QUANTIFIED EXPRESSION)))
(CALL 1. (E ERREND))
TAG10 (HRRZ@ 3. -1. P)
(HLRZ@ 3. 3.)
(HLRZ@ 2. -1. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PROPSUBST))
(HRRZ@ 2. 0. P)
(CALL 2. (E SPECALL))
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP TH1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(JUMPN 3. TAG2)
(MOVE 5. 4.)
(MOVEI 4. (QUOTE NIL))
(CALL 5. (E TH2))
(JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG5)
(HLRZ@ 1. -1. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG8)
(MOVE 2. -3. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG10)
(MOVE 1. -3. P)
(JRST 0. TAG9)
TAG10 (MOVE 2. -3. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E CONS))
TAG11
TAG9 (MOVE 4. 0. P)
(HRRZ@ 3. -1. P)
(MOVE 2. -2. P)
(CALL 4. (E TH1))
(JRST 0. TAG7)
TAG8 (MOVE 2. -2. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG16)
(MOVE 2. -2. P)
(JRST 0. TAG15)
TAG16 (MOVE 2. -2. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E CONS))
(MOVE 2. 1.)
TAG17
TAG15 (MOVE 4. 0. P)
(HRRZ@ 3. -1. P)
(MOVE 1. -3. P)
(CALL 4. (E TH1))
TAG13
TAG7 (JUMPN 1. TAG5)
(TDZA 1. 1.)
TAG5 (MOVEI 1. (QUOTE T))
TAG3
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP TH2 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(JUMPN 5. TAG2)
(CALL 4. (E TH))
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 5.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG3)
(MOVE 2. 3.)
(HLRZ@ 1. 5.)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG5)
(MOVE 3. -2. P)
(JRST 0. TAG4)
TAG5 (MOVE 2. -2. P)
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVE 3. 1.)
TAG6
TAG4 (HRRZ@ 5. 0. P)
(MOVE 4. -1. P)
(MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 5. (E TH2))
(JRST 0. TAG1)
TAG3 (MOVE 2. -1. P)
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG11)
(MOVE 4. -1. P)
(JRST 0. TAG10)
TAG11 (MOVE 2. -1. P)
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVE 4. 1.)
TAG12
TAG10 (HRRZ@ 5. 0. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 5. (E TH2))
TAG8
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(JUMPN 2. TAG2)
(JUMPE 4. TAG4)
(HRRZ@ 5. 4.)
(EXCH 4. 3.)
(MOVE 3. -2. P)
(EXCH 2. 1.)
(HLRZ@ 1. 0. P)
(CALL 5. (E THR))
(JUMPN 1. TAG3)
TAG4 (TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 5. 0. P)
(MOVE 4. -1. P)
(HRRZ@ 3. -2. P)
(MOVE 2. -3. P)
(HLRZ@ 1. -2. P)
(CALL 5. (E THL))
TAG5
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP THL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(MOVEI 2. (QUOTE NOT))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG2)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE AND))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG3)
(HRRZ@ 1. -4. P)
(CALL 1. (E BINAND))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. 1.)
(CALL 5. (E TH2L))
(JRST 0. TAG1)
TAG3 (MOVEI 2. (QUOTE OR))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG4)
(HRRZ@ 1. -4. P)
(CALL 1. (E BINOR))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(CALL 1. (E CADR))
(CALL 5. (E TH1L))
(JUMPE 1. TAG6)
(HRRZ@ 1. -4. P)
(CALL 1. (E BINOR))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(CALL 1. (E CADDR))
(CALL 5. (E TH1L))
(JUMPN 1. TAG5)
TAG6 (TDZA 1. 1.)
TAG5 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG4 (MOVEI 2. (QUOTE IMPLIES))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 1. (E CADR))
(CALL 5. (E TH1L))
(JUMPE 1. TAG9)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPN 1. TAG8)
TAG9 (TDZA 1. 1.)
TAG8 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG7 (MOVEI 2. (QUOTE EQUIVALENT))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG10)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 5. (E TH2L))
(JUMPE 1. TAG12)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 5. (E TH2R))
(JUMPN 1. TAG11)
TAG12 (TDZA 1. 1.)
TAG11 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG10 (MOVE 2. -1. P)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG13)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG13 (MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 0. P)
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(CALL 4. (E TH))
TAG14
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP THR SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(MOVEI 2. (QUOTE NOT))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG2)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1L))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE AND))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG3)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPE 1. TAG5)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 1. (E CADR))
(CALL 5. (E TH1R))
(JUMPN 1. TAG4)
TAG5 (TDZA 1. 1.)
TAG4 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG3 (MOVEI 2. (QUOTE OR))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG6)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 5. (E TH2R))
(JRST 0. TAG1)
TAG6 (MOVEI 2. (QUOTE IMPLIES))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 5. (E TH11))
(JRST 0. TAG1)
TAG7 (MOVEI 2. (QUOTE EQUIVALENT))
(HLRZ@ 1. -4. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG8)
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(CALL 5. (E TH11))
(JUMPE 1. TAG10)
(HRRZ@ 1. -4. P)
(CALL 1. (E REVERSE))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(CALL 5. (E TH11))
(JUMPN 1. TAG9)
TAG10 (TDZA 1. 1.)
TAG9 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG8 (MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG11)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG11 (MOVE 2. -1. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 0. P)
(MOVE 3. 1.)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 4. (E TH))
TAG12
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH1L SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 2. 4.)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
(MOVE 2. -3. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 0. P)
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(CALL 4. (E TH))
(JUMPN 1. TAG3)
(TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(MOVE 2. -2. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 0. P)
(MOVE 3. -1. P)
(MOVE 2. 1.)
(MOVE 1. -3. P)
(CALL 4. (E TH))
(JUMPN 1. TAG7)
(TDZA 1. 1.)
TAG7 (MOVEI 1. (QUOTE T))
TAG5
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH1R SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
(MOVE 2. -1. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 0. P)
(MOVE 3. 1.)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 4. (E TH))
(JUMPN 1. TAG3)
(TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 2. -2. P)
(MOVE 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(MOVE 2. 0. P)
(MOVE 1. -4. P)
(CALL 2. (E CONS))
(MOVE 4. 1.)
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 4. (E TH))
(JUMPN 1. TAG7)
(TDZA 1. 1.)
TAG7 (MOVEI 1. (QUOTE T))
TAG5
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH2L SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 2. 4.)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
(MOVE 2. -3. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1L))
(JUMPN 1. TAG3)
(TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(MOVE 2. -2. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. 1.)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1L))
(JUMPN 1. TAG7)
(TDZA 1. 1.)
TAG7 (MOVEI 1. (QUOTE T))
TAG5
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH2R SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
(MOVE 2. -1. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 0. P)
(MOVE 4. 1.)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPN 1. TAG3)
(TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 2. -2. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(MOVE 2. 0. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 1.)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPN 1. TAG7)
(TDZA 1. 1.)
TAG7 (MOVEI 1. (QUOTE T))
TAG5
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP TH11 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P 5.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 2. 4.)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG3)
(MOVE 2. -3. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(MOVE 2. 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPN 1. TAG3)
(TDZA 1. 1.)
TAG3 (MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG7)
(MOVE 2. -2. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(MOVE 5. 0. P)
(MOVE 4. -1. P)
(MOVE 3. 1.)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 5. (E TH1R))
(JUMPN 1. TAG7)
(TDZA 1. 1.)
TAG7 (MOVEI 1. (QUOTE T))
TAG5
TAG1 (SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP UNGEN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P 4.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVE 1. 3.)
(CALL 2. (E FREEIN))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE (VARIABLE FREE IN ASSUMPTIONS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. -2. P)
(CALL 1. (E USEDINEXISTSPEC))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE (USED IN EXISTENTIALLY SPECIFIED LINE)))
(CALL 1. (E ERREND))
TAG7 (CALL 0. (E GENSYM))
(MOVE 3. -4. P)
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(CALL 3. (E SUBST))
(MOVEM 1. -4. P)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG9)
(MOVEI 1. (QUOTE (VARIABLE CONFLICT)))
(CALL 1. (E ERREND))
TAG9 (MOVE 1. -1. P)
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE FORALL))
(CALL 2. (E XCONS))
(MOVE 3. -4. P)
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 3. (E SUBST))
(CALL 1. (E NCONS))
(POP P 2.)
(SUB P (C 0. 0. 5. 5.))
(JCALL 2. (E XCONS))
NIL
(LAP UNION SUBR)
(PUSH P 1.)
(JUMPE 1. TAG1)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG2)
(HLRZ@ 1. 0. P)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E UNION))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
TAG3
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP UNION2 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(JUMPN 1. TAG2)
(MOVE 1. 2.)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 1.)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG3)
(MOVE 2. 0. P)
(HRRZ@ 1. -1. P)
(CALL 2. (E UNION2))
(JRST 0. TAG1)
TAG3 (MOVE 2. 0. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E CONS))
(MOVE 2. 1.)
(HRRZ@ 1. -1. P)
(CALL 2. (E UNION2))
TAG4
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP USEDINEXISTSPEC SUBR)
(PUSH P 1.)
(CALL 0. (E CURTEXT))
(PUSH P 1.)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG3)
(CALL 1. (E CADDAR))
(MOVEI 2. (QUOTE ES))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG7)
(HLRZ@ 1. 0. P)
(CALL 1. (E CADR))
(CALL 1. (E FREEVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG2)
TAG7 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP USEDVAR SUBR)
(PUSH P 1.)
(CALL 0. (E CURTEXT))
(PUSH P 1.)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG3)
(CALL 1. (E CADAR))
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG2)
TAG7 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP VALID SUBR)
(MOVEI 2. (QUOTE INVALID))
(JCALL 2. (E NEQ))
NIL
(LAP WFFLIST SUBR)
(MOVE 2. 1.)
(MOVEI 1. (QUOTE WFFPART))
(JCALL 2. (E MAPCAR))
NIL
(LAP WFFPART SUBR)
(CALL 1. (E GETLINE))
(JCALL 1. (E CADR))
NIL
(LAP GETINFXNAM SUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG5)
(MOVE 1. -1. P)
(JRST 0. TAG1)
TAG5 (MOVEI 2. (QUOTE INFXNAM))
(MOVE 1. -1. P)
(CALL 2. (E SEEKPROP))
(MOVEM 1. 0. P)
(JUMPE 1. TAG7)
(CALL 1. (E CADR))
(JRST 0. TAG1)
TAG7 (MOVE 1. -1. P)
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP INFX SUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(CALL 3. (E INFXEXPR))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INFXARGS SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE /())
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG6)
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 3. (E INFXEXPR))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG6 (MOVE 2. -2. P)
(MOVEI 1. (QUOTE *COMMA*))
(CALL 2. (E CONS))
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(CALL 3. (E INFXPARENED))
TAG10
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(PUTPROP (QUOTE INFXATOM) (QUOTE PRNTATOM) (QUOTE EXPR))
(LAP INFXCOND SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE IF))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(HRRZ@ 1. 0. P)
(CALL 1. (E CAAR))
(CALL 3. (E INFXEXPR))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE THEN))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADAR))
(CALL 3. (E INFXEXPR))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(JUMPE 1. TAG2)
(MOVEI 1. (QUOTE ELSE))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E INFXATOM))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(CALL 1. (E CADR))
(CALL 3. (E INFXEXPR))
TAG2 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INFXFUN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. -2. P)
(CALL 1. (E INFXATOM))
(JRST 0. TAG1)
TAG2 (MOVE 3. 0. P)
(MOVE 2. -1. P)
(MOVE 1. -2. P)
(CALL 3. (E INFXPARENED))
TAG3
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP INFXEXPR SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E ATOM))
(JUMPE 1. TAG6)
(MOVE 1. -3. P)
(CALL 1. (E INFXATOM))
(JRST 0. TAG2)
TAG6 (HLRZ@ 1. -3. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG1)
(MOVEI 2. (QUOTE INFXFUN))
(HLRZ@ 1. -3. P)
(CALL 2. (E GETGET))
(MOVEM 1. 0. P)
(JUMPE 1. TAG9)
(PUSH P (C 0. 0. TAG10 0.))
(CALL 1. (E CADR))
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 1. (E NCONS))
(MOVE 2. -4. P)
(CALL 2. (E XCONS))
(MOVE 2. -5. P)
(CALL 2. (E XCONS))
(PUSH P 1.)
(MOVNI 6. 2.)
(JCALL 14. (E APPLY))
TAG10 (JRST 0. TAG2)
TAG9
TAG1 (MOVE 3. -1. P)
(MOVE 2. -2. P)
(HLRZ@ 1. -3. P)
(CALL 3. (E INFXFUN))
(MOVE 3. -1. P)
(MOVEI 2. (QUOTE 10000.))
(HRRZ@ 1. -3. P)
(CALL 3. (E INFXARGS))
(MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INFXLIST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 4.)
(MOVEI 2. (QUOTE PREC))
(CALL 2. (E GET))
(PUSH P 1.)
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG3)
(MOVE 1. -3. P)
(CALL 1. (E INFXATOM))
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(PUSH P 1.)
(HRRZ@ 1. -4. P)
(JUMPN 1. TAG7)
(MOVE 3. -3. P)
(JRST 0. TAG6)
TAG7 (HLRZ@ 3. -2. P)
TAG8
TAG6 (MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E INFXEXPR))
(SUB P (C 0. 0. 1. 1.))
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INFXOPER SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVEI 2. (QUOTE PREC))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(MOVE 2. -2. P)
(HLRZ@ 1. 1.)
(CALL 2. (E *LESS))
(JUMPN 1. TAG6)
(MOVE 2. -1. P)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E *LESS))
(JUMPE 1. TAG5)
TAG6 (MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 3. (E INFXPARENED))
(JRST 0. TAG1)
TAG5 (HRRZ@ 1. -3. P)
(JUMPN 1. TAG8)
(HLRZ@ 1. -3. P)
(CALL 1. (E INFXATOM))
(JRST 0. TAG1)
TAG8 (HRRZ@ 1. -3. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG10)
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(HRRZ@ 2. -3. P)
(HLRZ@ 1. -3. P)
(CALL 4. (E INFXLIST))
(JRST 0. TAG1)
TAG10 (HLRZ@ 3. 0. P)
(MOVE 2. -2. P)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 3. (E INFXEXPR))
(MOVE 4. -1. P)
(MOVE 3. -2. P)
(HRRZ@ 2. -3. P)
(HRRZ@ 2. 2.)
(HLRZ@ 1. -3. P)
(CALL 4. (E INFXLIST))
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INFXPARENED SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE /())
(CALL 1. (E INFXATOM))
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(MOVE 1. 0. P)
(CALL 3. (E INFXEXPR))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INFXQUOTE SUBR)
(PUSH P 1.)
(MOVEI 1. (QUOTE QUOTE))
(CALL 1. (E INFXATOM))
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 1. (E PRIN1))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INFXSPEC SUBR)
(PUSH P 2.)
(MOVEI 2. (QUOTE SPECOPER))
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(EXCH 2. -1. P)
(EXCH 1. 0. P)
(CALLF@ 3. 0. P)
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP PRNTATOM SUBR)
(PUSH P 1.)
(CALL 1. (E GETINFXNAM))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *PLUS))
(POP P 2.)
(CALL 2. (E *GREAT))
(JUMPE 1. TAG5)
(CALL 0. (E TERPRI))
TAG5 (MOVE 1. 0. P)
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(PUTPROP (QUOTE PREC) (QUOTE INFXOPER) (QUOTE INFXFUN))
(PUTPROP (QUOTE SPECOPER) (QUOTE INFXSPEC) (QUOTE INFXFUN))
(PUTPROP (QUOTE COND) (QUOTE INFXCOND) (QUOTE SPECOPER))
(PUTPROP (QUOTE QUOTE) (QUOTE INFXQUOTE) (QUOTE SPECOPER))
(LAP SUBFUN1FITSLINE SUBR)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. (SPECIAL EXPEXP))
(JCALL 3. (E INFXEXPR))
NIL
(LAP FITSLINE SUBR)
(JSP 6. SPECBIND)
(0. 0. (SPECIAL EXPEXP))
(0. 0. (SPECIAL EXPLGTH))
(0. 0. (SPECIAL EXPLIM))
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E ATOM))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG5 (MOVEI 1. (QUOTE 0.))
(MOVEM 1. (SPECIAL EXPLGTH))
(MOVE 1. -3. P)
(MOVEM 1. (SPECIAL EXPEXP))
(MOVEI 1. (QUOTE NIL))
(CALL 1. (E LINELENGTH))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 2. (E *PLUS))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E *DIF))
(MOVEM 1. (SPECIAL EXPLIM))
(MOVEI 3. (QUOTE EXPR))
(MOVEI 2. (QUOTE LGTHATOM))
(MOVEI 1. (QUOTE INFXATOM))
(CALL 3. (E INITPROP))
(MOVEI 1. (QUOTE ((SUBFUN1FITSLINE))))
(CALL 15. (E ERRSET))
(MOVEI 2. (QUOTE EXPR))
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE INFXATOM))
(CALL 2. (E DELETEPROP))
(MOVE 1. 0. P)
TAG1 (SUB P (C 0. 0. 4. 4.))
(JRST 0. SPECSTR)
NIL
(LAP LGTHATOM SUBR)
(PUSH P 1.)
(PUSH P (SPECIAL EXPLGTH))
(CALL 1. (E GETINFXNAM))
(CALL 1. (E FLATSIZE))
(POP P 2.)
(CALL 2. (E *PLUS))
(MOVEM 1. (SPECIAL EXPLGTH))
(MOVE 2. (SPECIAL EXPLIM))
(CALL 2. (E LEQ))
(JUMPN 1. TAG2)
(CLEARM 1. (SPECIAL EXPLGTH))
(CALL 0. (E ERR))
TAG2 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP TDD SUBR)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 1.))
(JCALL 3. (E TDDEXP))
NIL
(LAP TDDARGS SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPE 1. TAG2)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(HLRZ@ 1. -2. P)
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 2. (E *PLUS))
(MOVE 3. -1. P)
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E TDDEXP))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG2 (MOVEI 1. (QUOTE /())
(CALL 1. (E INFXATOM))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. -2. P)
(CALL 3. (E TDDLIST))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE NIL))
TAG7
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP TDDEXP SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 2.)
(CALL 1. (E TABTO))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 3. (E FITSLINE))
(JUMPE 1. TAG6)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 0.))
(MOVE 1. -3. P)
(CALL 3. (E INFXEXPR))
(JRST 0. TAG2)
TAG6 (MOVEI 2. (QUOTE TDDFUN))
(HLRZ@ 1. -3. P)
(CALL 2. (E GETGET))
(MOVEM 1. 0. P)
(JUMPE 1. TAG8)
(PUSH P (C 0. 0. TAG9 0.))
(CALL 1. (E CADR))
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 1. (E NCONS))
(MOVE 2. -4. P)
(CALL 2. (E XCONS))
(MOVE 2. -5. P)
(CALL 2. (E XCONS))
(PUSH P 1.)
(MOVNI 6. 2.)
(JCALL 14. (E APPLY))
TAG9 (JRST 0. TAG2)
TAG8
TAG1 (MOVE 3. -1. P)
(MOVE 2. -2. P)
(HLRZ@ 1. -3. P)
(CALL 3. (E TDDFUNC))
(HRRZ@ 1. -3. P)
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVE 3. -2. P)
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E TDDARGS))
(MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP TDDFUNC SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG5)
(MOVE 1. -2. P)
(CALL 1. (E INFXATOM))
(JRST 0. TAG1)
TAG5 (MOVEI 1. (QUOTE /())
(CALL 1. (E INFXATOM))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. -2. P)
(CALL 3. (E TDDEXP))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E INFXATOM))
(MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP TDDLIST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG3)
(HLRZ@ 1. 1.)
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(MOVE 2. -2. P)
(POP P 1.)
(CALL 3. (E TDDEXP))
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE /,))
(CALL 1. (E INFXATOM))
TAG7 (JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP TDDINFX SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HRRZ@ 1. 1.)
(JUMPE 1. TAG7)
(HRRZ@ 1. -5. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG6)
TAG7 (MOVE 1. -5. P)
(CALL 1. (E INFX))
(JRST 0. TAG2)
TAG6 (HLRZ@ 1. -5. P)
(MOVEM 1. -2. P)
(HLRZ@ 1. -5. P)
(CALL 1. (E GETINFXNAM))
(CALL 1. (E FLATSIZE))
(MOVE 3. -3. P)
(MOVE 2. -4. P)
(MOVEM 1. -1. P)
(HRRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 3. (E TDDEXP))
(HRRZ@ 1. -5. P)
(HRRZ@ 1. 1.)
(MOVEM 1. 0. P)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG3)
(CALL 0. (E TERPRI))
(MOVE 1. -4. P)
(CALL 1. (E TABTO))
(MOVE 1. -2. P)
(CALL 1. (E INFXATOM))
(HLRZ@ 1. 0. P)
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -5. P)
(CALL 2. (E *PLUS))
(MOVE 3. -4. P)
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E TDDEXP))
(HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 6. 6.))
(POPJ P)
NIL
(PUTPROP (QUOTE PREC) (QUOTE TDDINFX) (QUOTE TDDFUN))
(LAP ALLFIT SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPN 1. TAG6)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG2)
TAG6
TAG1 (HRRZ@ 1. -2. P)
(JUMPN 1. TAG8)
(HLRZ@ 1. -2. P)
(CALL 1. (E FLATSIZE))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E LEQ))
(JRST 0. TAG2)
TAG8 (HLRZ@ 1. -2. P)
(CALL 1. (E FLATSIZE))
(MOVE 2. -1. P)
(CALL 2. (E *GREAT))
(JUMPN 1. TAG3)
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP PRINL SUBR)
(PUSH P 1.)
(JUMPE 1. TAG1)
(CALL 0. (E CHRCT))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 2.))
(CALL 2. (E *PLUS))
(POP P 2.)
(CALL 2. (E *GREAT))
(JUMPE 1. TAG2)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(MOVE 1. 0. P)
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 0. P)
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E PRINL))
(MOVEI 1. (QUOTE NIL))
TAG6
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP PRINS SUBR)
(PUSH P 1.)
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP PRINTEXPR SUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE 0.))
(MOVEI 2. (QUOTE 1.))
(CALL 3. (E PRINTSUBEXPR))
(CALL 0. (E TERPRI))
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP PRINTLIST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVEI 1. (QUOTE /())
(CALL 1. (E PRINC))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. -2. P)
(CALL 3. (E PRINTMEMBERS))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP PRINTMEMBERS SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG3)
(CALL 1. (E ATOM))
(JUMPE 1. TAG7)
(MOVEI 1. (QUOTE / /./ ))
(CALL 1. (E PRINC))
(MOVE 1. -2. P)
(CALL 1. (E PRIN1))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG2)
TAG7 (HLRZ@ 1. -2. P)
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(JUMPN 1. TAG12)
(MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(JRST 0. TAG11)
TAG12 (HRRZ@ 1. -3. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG13)
(MOVEI 2. (QUOTE 4.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(JRST 0. TAG11)
TAG13 (MOVEI 3. (QUOTE 0.))
TAG14
TAG11 (MOVE 2. -2. P)
(POP P 1.)
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP PRINTSUBEXPR SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 2.)
(CALL 1. (E TABTO))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVE 1. -3. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG5)
(MOVE 1. -3. P)
(CALL 1. (E PRIN1))
(JRST 0. TAG1)
TAG5 (HLRZ@ 1. -3. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG7)
(HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG7)
(MOVEI 2. (QUOTE PPROP))
(HLRZ@ 1. -3. P)
(CALL 2. (E GETGET))
(MOVEM 1. 0. P)
TAG7 (MOVE 1. 0. P)
(JUMPE 1. TAG10)
(CALL 1. (E CADR))
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVE 1. -4. P)
(CALLF@ 3. 0. P)
(SUB P (C 0. 0. 1. 1.))
(JRST 0. TAG1)
TAG10 (MOVE 1. -3. P)
(CALL 1. (E FLATSIZE))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(MOVE 2. -2. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E LEQ))
(JUMPE 1. TAG12)
(MOVE 1. -3. P)
(CALL 1. (E PRIN1))
(JRST 0. TAG1)
TAG12 (HLRZ@ 1. -3. P)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 4.))
(CALL 2. (E LEQ))
(JUMPN 1. TAG15)
(HRRZ@ 1. -3. P)
(PUSH P 1.)
(CALL 0. (E CHRCT))
(PUSH P 1.)
(HLRZ@ 1. -5. P)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 2.))
(CALL 2. (E *PLUS))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E *DIF))
(MOVE 3. -2. P)
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E ALLFIT))
(JUMPE 1. TAG14)
TAG15 (MOVEI 1. (QUOTE /())
(CALL 1. (E PRINC))
(HLRZ@ 1. -3. P)
(CALL 1. (E PRIN1))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(HRRZ@ 1. -3. P)
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE 1.))
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E PRINTMEMBERS))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
(JRST 0. TAG1)
TAG14 (MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 3. (E PRINTLIST))
(MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP PRINTN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P (C 0. 0. (QUOTE 1.) 0.))
TAG1 (MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E *LESS))
(JUMPE 1. TAG6)
(MOVE 1. -1. P)
(JRST 0. TAG2)
TAG6 (MOVE 1. -2. P)
(CALL 1. (E PRINC))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. 0. P)
(CALL 2. (E *PLUS))
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP PRINTNOCRFUN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 1. (E FLATSIZE))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(MOVE 2. -1. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E LEQ))
(JUMPE 1. TAG5)
(MOVE 1. -2. P)
(CALL 1. (E PRIN1))
(JRST 0. TAG1)
TAG5 (MOVEI 1. (QUOTE /())
(CALL 1. (E PRINC))
(HLRZ@ 1. -2. P)
(CALL 1. (E PRIN1))
(MOVEI 1. (QUOTE / ))
(CALL 1. (E PRINC))
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E PRINC))
(HRRZ@ 1. -2. P)
(HRRZ@ 1. 1.)
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 2. (E *PLUS))
(MOVEI 2. (QUOTE 1.))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 2. (E *PLUS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E PRINTMEMBERS))
(MOVEI 1. (QUOTE /)))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP TABTO SUBR)
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVE 2. 0. P)
(CALL 2. (E *GREAT))
(JUMPE 1. TAG5)
(CALL 0. (E TERPRI))
TAG5 (CALL 0. (E CURCOL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E *DIF))
(PUSH P 1.)
(MOVEI 1. (QUOTE 3.))
(CALL 1. (E MINUS))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E LSH))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE / ))
(CALL 2. (E PRINTN))
(CALL 0. (E CURCOL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE / ))
(CALL 2. (E PRINTN))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(PUTPROP (QUOTE NOCR) (QUOTE PRINTNOCRFUN) (QUOTE PPROP))
(FLAG (QUOTE (ADDAXIOM ADDSCHEMA ADDTHEOREM DEFPROP GIVEAX GIVEPROOF GIVESCHM MAKETHM SETQ USEAX USESCHM)) (QUOT~
E NOCR))
(PROG2 (SETQ PRECLIS* (CONS (QUOTE IMPLIES) PRECLIS*)) (MKPREC))
(PROG2 (SETQ PRECLIS* (CONS (QUOTE EQUIVALENT) PRECLIS*)) (MKPREC))
(PRECSET (QUOTE CMAPS) (QUOTE LESSP))
(PRECSET (QUOTE CONTAINED) (QUOTE LESSP))
(PRECSET (QUOTE INTERSECTION) (QUOTE CONTAINED))
(PRECSET (QUOTE MAPS) (QUOTE INTERSECTION))
(PRECSET (QUOTE MEMBER) (QUOTE LESSP))
(PRECSET (QUOTE PRODUCT) (QUOTE INTERSECTION))
(PRECSET (QUOTE UNION) (QUOTE CONTAINED))
(PUTPROP (QUOTE &) (QUOTE (NIL AND NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ⊂) (QUOTE (NIL CONTAINED NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE =) (QUOTE (> EQUAL IMPLIES)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ≡) (QUOTE (NIL EQUIVALENT NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ∀) (QUOTE (NIL FORALL NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ≥) (QUOTE (NIL GEQ NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ∩) (QUOTE (NIL INTERSECTION NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE →) (QUOTE (→ MAPS CMAPS)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ⊃) (QUOTE (NIL IMPLIES NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ≤) (QUOTE (NIL LEQ NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ε) (QUOTE (NIL MEMBER NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ≠) (QUOTE (NIL NEQ NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ⊗) (QUOTE (NIL PRODUCT NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ∃) (QUOTE (NIL THEREEXISTS NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ∪) (QUOTE (NIL UNION NIL)) (QUOTE SWITCH*))
(PUTPROP (QUOTE ALL) (QUOTE FORALL) (QUOTE NEWNAM))
(PUTPROP (QUOTE EXISTS) (QUOTE THEREEXISTS) (QUOTE NEWNAM))
(PUTPROP (QUOTE EQU) (QUOTE EQUIVALENT) (QUOTE NEWNAM))
(PUTPROP (QUOTE GREATEQ) (QUOTE GEQ) (QUOTE NEWNAM))
(PUTPROP (QUOTE IMP) (QUOTE IMPLIES) (QUOTE NEWNAM))
(PUTPROP (QUOTE LESSEQ) (QUOTE LEQ) (QUOTE NEWNAM))
(PUTPROP (QUOTE MEM) (QUOTE MEMBER) (QUOTE NEWNAM))
(LETTER 3.)
(REMPROP (QUOTE LAMBDA) (QUOTE STAT))
(REMPROP (QUOTE GO) (QUOTE STAT))
(REMPROP (QUOTE STEP) (QUOTE DELIM))
(REMPROP (QUOTE DO) (QUOTE DELIM))
(REMPROP (QUOTE MAP) (QUOTE NEWFORM))
(REMPROP (QUOTE MAPLIST) (QUOTE NEWFORM))
(REMPROP (QUOTE MAPCAR) (QUOTE NEWFORM))
(REMPROP (QUOTE EXPLODE) (QUOTE NEWNAM))
(SETQ IGLIST* (QUOTE (9. 10. 12. 13. 32.)))
(PUTPROP (QUOTE EXPR) (QUOTE PROCDEF) (QUOTE STAT))
(SETQ LOGICALCONSTANTS (QUOTE (TRUE FALSE)))
(SETQ QUANTIFIERS (QUOTE (FORALL LAMBDA THEREEXISTS)))
(SETQ DDWIDTH 84.)
(SETQ FILEWIDTH 69.)
(SETQ IIIWIDTH 88.)
(SETQ IMLACWIDTH 80.)
(SETQ TTYWIDTH 71.)